p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
rv-disjoint(p;n;X;Y)  (E(n;X * Y) = (E(n;X) * E(n;Y))  ) 

latex

Definitions

n - m, n+m, -n, i  j , FinProbSpace, E(n;F), rv-disjoint(p;n;X;Y), RandomVariable(p;n), , {x:A| B(x)} , False, Void, a < b, A  B, left + right, Unit, P  Q, P & Q, x:A  B(x), P  Q, x:AB(x), (i = j), , b, A, b, , , t  T, #$n, x:A. B(x), s = t, , <a, b>, weighted-sum(p;F), r * s, X * Y, f(a), null, ||as||, {i..j}, S  T, type List, Top, x:A.B(x), P  Q, x.A(x), rv-shift(x;X), x,y:A//B(x;y), SQType(T), {T}, s ~ t, , Outcome, T, True, r + s, cons-seq(x;s), suptype(S; T), i  j < k, Type, P  Q

Lemmas

qmul comm qrng, qmul zero qrng, ws-linear, mon ident q, qadd comm q, cons-seq wf, rv-disjoint-shift, int inc rationals, qadd wf, natural number wf p-outcome, true wf, squash wf, ws-constant, p-outcome wf, rv-shift wf, expectation wf, weighted-sum wf2, rv-mul wf, rv-disjoint-rv-shift, rationals wf, top wf, length wf nat, int seg wf, null-seq wf, qmul wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, le wf, random-variable wf, rv-disjoint wf, nat wf, finite-prob-space wf, nat properties, ge wf